(*----------------------------------------------------------------------(C)-*)
(* Copyright (C) 2006-2012 Konstantin Korovin and The University of Manchester. 
   This file is part of iProver - a theorem prover for first-order logic.

   iProver is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   (at your option) any later version.
   iProver is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  
   See the GNU General Public License for more details.
   You should have received a copy of the GNU General Public License
   along with iProver.  If not, see <http://www.gnu.org/licenses/>.         *)
(*----------------------------------------------------------------------[C]-*)





<html><body>
<pre><font color="990000">(*</font>
<font color="990000"> * Heap: heaps implemented both functionally and imperatively</font>
<font color="990000"> * Copyright (C) 2003 Jean-Christophe FILLIATRE</font>
<font color="990000"> * </font>
<font color="990000"> * This software is free software; you can redistribute it and/or</font>
<font color="990000"> * modify it under the terms of the GNU Library General Public</font>
<font color="990000"> * License version 2, as published by the Free Software Foundation.</font>
<font color="990000"> * </font>
<font color="990000"> * This software is distributed in the hope that it will be useful,</font>
<font color="990000"> * but WITHOUT ANY WARRANTY; without even the implied warranty of</font>
<font color="990000"> * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.</font>
<font color="990000"> * </font>
<font color="990000"> * See the GNU Library General Public License version 2 for more details</font>
<font color="990000"> * (enclosed in the file LGPL).</font>
<font color="990000"> *)</font>

<font color="990000">(*s Heaps *)</font>

<font color="green">module</font> <font color="green">type</font> <font color="0033cc">Ordered</font> = <font color="990099">sig</font>
  <font color="green">type</font> t
  <font color="green">val</font> compare : t -> t -> int
<font color="990099">end</font>

<font color="green">exception</font> <font color="0033cc">EmptyHeap</font>

<font color="990000">(*s Imperative implementation *)</font>

<font color="green">module</font> <font color="0033cc">Imperative</font>(<font color="0033cc">X</font> : <font color="0033cc">Ordered</font>) = <font color="990099">struct</font>

  <font color="990000">(* The heap is encoded in the array [data], where elements are stored</font>
<font color="990000">     from [0] to [size - 1]. From an element stored at [i], the left </font>
<font color="990000">     (resp. right) subtree, if any, is rooted at [2*i+1] (resp. [2*i+2]). *)</font>

  <font color="green">type</font> t = { <font color="green">mutable</font> size : int; <font color="green">mutable</font> data : <font color="0033cc">X</font>.t array }

  <font color="990000">(* When [create n] is called, we cannot allocate the array, since there is</font>
<font color="990000">     no known value of type [X.t]; we'll wait for the first addition to </font>
<font color="990000">     do it, and we remember this situation with a negative size. *)</font>

  <font color="green">let</font> create n = 
    <font color="77aaaa">if</font> n <= 0 <font color="77aaaa">then</font> invalid_arg <font color="aa4444">"create"</font>;
    { size = -n; data = [<font color="77aaaa">||</font>] }

  <font color="green">let</font> is_empty h = h.size <= 0

  <font color="990000">(* [resize] doubles the size of [data] *)</font>

  <font color="green">let</font> resize h =
    <font color="green">let</font> n = h.size <font color="green">in</font>
    <font color="cc9900">assert</font> (n > 0);
    <font color="green">let</font> n' = 2 * n <font color="green">in</font>
    <font color="green">let</font> d = h.data <font color="green">in</font>
    <font color="green">let</font> d' = <font color="0033cc">Array</font>.create n' d.(0) <font color="green">in</font>
    <font color="0033cc">Array</font>.blit d 0 d' 0 n;
    h.data <- d'

  <font color="green">let</font> add h x =
    <font color="990000">(* first addition: we allocate the array *)</font>
    <font color="77aaaa">if</font> h.size < 0 <font color="77aaaa">then</font> <font color="990099">begin</font>
      h.data <- <font color="0033cc">Array</font>.create (- h.size) x; h.size <- 0
    <font color="990099">end</font>;
    <font color="green">let</font> n = h.size <font color="green">in</font>
    <font color="990000">(* resizing if needed *)</font>
    <font color="77aaaa">if</font> n == <font color="0033cc">Array</font>.length h.data <font color="77aaaa">then</font> resize h;
    <font color="green">let</font> d = h.data <font color="green">in</font>
    <font color="990000">(* moving [x] up in the heap *)</font>
    <font color="green">let</font> <font color="green">rec</font> moveup i =
      <font color="green">let</font> fi = (i - 1) / 2 <font color="green">in</font>
      <font color="77aaaa">if</font> i > 0 <font color="77aaaa">&&</font> <font color="0033cc">X</font>.compare d.(fi) x < 0 <font color="77aaaa">then</font> <font color="990099">begin</font>
	d.(i) <- d.(fi);
	moveup fi
      <font color="990099">end</font> <font color="77aaaa">else</font>
	d.(i) <- x
    <font color="green">in</font>
    moveup n;
    h.size <- n + 1

  <font color="green">let</font> maximum h =
    <font color="77aaaa">if</font> h.size <= 0 <font color="77aaaa">then</font> <font color="red">raise</font> <font color="0033cc">EmptyHeap</font>;
    h.data.(0)

  <font color="green">let</font> remove h =
    <font color="77aaaa">if</font> h.size <= 0 <font color="77aaaa">then</font> <font color="red">raise</font> <font color="0033cc">EmptyHeap</font>;
    <font color="green">let</font> n = h.size - 1 <font color="green">in</font>
    h.size <- n;
    <font color="green">let</font> d = h.data <font color="green">in</font>
    <font color="green">let</font> x = d.(n) <font color="green">in</font>
    <font color="990000">(* moving [x] down in the heap *)</font>
    <font color="green">let</font> <font color="green">rec</font> movedown i =
      <font color="green">let</font> j = 2 * i + 1 <font color="green">in</font>
      <font color="77aaaa">if</font> j < n <font color="77aaaa">then</font>
	<font color="green">let</font> j = 
	  <font color="green">let</font> j' = j + 1 <font color="green">in</font> 
	  <font color="77aaaa">if</font> j' < n <font color="77aaaa">&&</font> <font color="0033cc">X</font>.compare d.(j') d.(j) > 0 <font color="77aaaa">then</font> j' <font color="77aaaa">else</font> j 
	<font color="green">in</font>
	<font color="77aaaa">if</font> <font color="0033cc">X</font>.compare d.(j) x > 0 <font color="77aaaa">then</font> <font color="990099">begin</font> 
	  d.(i) <- d.(j); 
	  movedown j 
	<font color="990099">end</font> <font color="77aaaa">else</font>
	  d.(i) <- x
      <font color="77aaaa">else</font>
	d.(i) <- x
    <font color="green">in</font>
    movedown 0

  <font color="green">let</font> pop_maximum h = <font color="green">let</font> m = maximum h <font color="green">in</font> remove h; m

  <font color="green">let</font> iter f h = 
    <font color="green">let</font> d = h.data <font color="green">in</font>
    <font color="77aaaa">for</font> i = 0 <font color="77aaaa">to</font> h.size - 1 <font color="77aaaa">do</font> f d.(i) <font color="77aaaa">done</font>

  <font color="green">let</font> fold f h x0 =
    <font color="green">let</font> n = h.size <font color="green">in</font>
    <font color="green">let</font> d = h.data <font color="green">in</font>
    <font color="green">let</font> <font color="green">rec</font> foldrec x i =
      <font color="77aaaa">if</font> i >= n <font color="77aaaa">then</font> x <font color="77aaaa">else</font> foldrec (f d.(i) x) (succ i)
    <font color="green">in</font>
    foldrec x0 0

<font color="990099">end</font>


<font color="990000">(*s Functional implementation *)</font>

<font color="green">module</font> <font color="green">type</font> <font color="0033cc">FunctionalSig</font> = <font color="990099">sig</font>
  <font color="green">type</font> elt
  <font color="green">type</font> t
  <font color="green">val</font> empty : t
  <font color="green">val</font> add : elt -> t -> t
  <font color="green">val</font> maximum : t -> elt
  <font color="green">val</font> remove : t -> t
  <font color="green">val</font> iter : (elt -> unit) -> t -> unit
  <font color="green">val</font> fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
<font color="990099">end</font>

<font color="green">module</font> <font color="0033cc">Functional</font>(<font color="0033cc">X</font> : <font color="0033cc">Ordered</font>) = <font color="990099">struct</font>

  <font color="990000">(* Heaps are encoded as complete binary trees, i.e., binary trees</font>
<font color="990000">     which are full expect, may be, on the bottom level where it is filled </font>
<font color="990000">     from the left. </font>
<font color="990000">     These trees also enjoy the heap property, namely the value of any node </font>
<font color="990000">     is greater or equal than those of its left and right subtrees.</font>
<font color="990000"></font>
<font color="990000">     There are 4 kinds of complete binary trees, denoted by 4 constructors:</font>
<font color="990000">     [FFF] for a full binary tree (and thus 2 full subtrees);</font>
<font color="990000">     [PPF] for a partial tree with a partial left subtree and a full</font>
<font color="990000">     right subtree;</font>
<font color="990000">     [PFF] for a partial tree with a full left subtree and a full right subtree</font>
<font color="990000">     (but of different heights);</font>
<font color="990000">     and [PFP] for a partial tree with a full left subtree and a partial</font>
<font color="990000">     right subtree. *)</font>

  <font color="green">type</font> elt = <font color="0033cc">X</font>.t

  <font color="green">type</font> t = 
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font>
    <font color="77aaaa">|</font> <font color="0033cc">FFF</font> <font color="green">of</font> t * <font color="0033cc">X</font>.t * t <font color="990000">(* full    (full,    full) *)</font>
    <font color="77aaaa">|</font> <font color="0033cc">PPF</font> <font color="green">of</font> t * <font color="0033cc">X</font>.t * t <font color="990000">(* partial (partial, full) *)</font>
    <font color="77aaaa">|</font> <font color="0033cc">PFF</font> <font color="green">of</font> t * <font color="0033cc">X</font>.t * t <font color="990000">(* partial (full,    full) *)</font>
    <font color="77aaaa">|</font> <font color="0033cc">PFP</font> <font color="green">of</font> t * <font color="0033cc">X</font>.t * t <font color="990000">(* partial (full,    partial) *)</font>

  <font color="green">let</font> empty = <font color="0033cc">Empty</font>
 
  <font color="990000">(* smart constructors for insertion *)</font>
  <font color="green">let</font> p_f l x r = <font color="77aaaa">match</font> l <font color="77aaaa">with</font>
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font> <font color="77aaaa">|</font> <font color="0033cc">FFF</font> _ -> <font color="0033cc">PFF</font> (l, x, r)
    <font color="77aaaa">|</font> _ -> <font color="0033cc">PPF</font> (l, x, r)

  <font color="green">let</font> pf_ l x = <font color="green">function</font>
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font> <font color="77aaaa">|</font> <font color="0033cc">FFF</font> _ <font color="green">as</font> r -> <font color="0033cc">FFF</font> (l, x, r)
    <font color="77aaaa">|</font> r -> <font color="0033cc">PFP</font> (l, x, r)

  <font color="green">let</font> <font color="green">rec</font> add x = <font color="green">function</font>
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font> -> 
	<font color="0033cc">FFF</font> (<font color="0033cc">Empty</font>, x, <font color="0033cc">Empty</font>)
    <font color="990000">(* insertion to the left *)</font>
    <font color="77aaaa">|</font> <font color="0033cc">FFF</font> (l, y, r) <font color="77aaaa">|</font> <font color="0033cc">PPF</font> (l, y, r) ->
	<font color="77aaaa">if</font> <font color="0033cc">X</font>.compare x y > 0 <font color="77aaaa">then</font> p_f (add y l) x r <font color="77aaaa">else</font> p_f (add x l) y r
    <font color="990000">(* insertion to the right *)</font>
    <font color="77aaaa">|</font> <font color="0033cc">PFF</font> (l, y, r) <font color="77aaaa">|</font> <font color="0033cc">PFP</font> (l, y, r) ->
	<font color="77aaaa">if</font> <font color="0033cc">X</font>.compare x y > 0 <font color="77aaaa">then</font> pf_ l x (add y r) <font color="77aaaa">else</font> pf_ l y (add x r)

  <font color="green">let</font> maximum = <font color="green">function</font>
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font> -> <font color="red">raise</font> <font color="0033cc">EmptyHeap</font>
    <font color="77aaaa">|</font> <font color="0033cc">FFF</font> (_, x, _) <font color="77aaaa">|</font> <font color="0033cc">PPF</font> (_, x, _) <font color="77aaaa">|</font> <font color="0033cc">PFF</font> (_, x, _) <font color="77aaaa">|</font> <font color="0033cc">PFP</font> (_, x, _) -> x

  <font color="990000">(* smart constructors for removal; note that they are different</font>
<font color="990000">     from the ones for insertion! *)</font>
  <font color="green">let</font> p_f l x r = <font color="77aaaa">match</font> l <font color="77aaaa">with</font>
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font> <font color="77aaaa">|</font> <font color="0033cc">FFF</font> _ -> <font color="0033cc">FFF</font> (l, x, r)
    <font color="77aaaa">|</font> _ -> <font color="0033cc">PPF</font> (l, x, r)

  <font color="green">let</font> pf_ l x = <font color="green">function</font>
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font> <font color="77aaaa">|</font> <font color="0033cc">FFF</font> _ <font color="green">as</font> r -> <font color="0033cc">PFF</font> (l, x, r)
    <font color="77aaaa">|</font> r -> <font color="0033cc">PFP</font> (l, x, r)

  <font color="green">let</font> <font color="green">rec</font> remove = <font color="green">function</font>
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font> -> 
	<font color="red">raise</font> <font color="0033cc">EmptyHeap</font>
    <font color="77aaaa">|</font> <font color="0033cc">FFF</font> (<font color="0033cc">Empty</font>, _, <font color="0033cc">Empty</font>) -> 
	<font color="0033cc">Empty</font>
    <font color="77aaaa">|</font> <font color="0033cc">PFF</font> (l, _, <font color="0033cc">Empty</font>) ->
	l
    <font color="990000">(* remove on the left *)</font>
    <font color="77aaaa">|</font> <font color="0033cc">PPF</font> (l, x, r) <font color="77aaaa">|</font> <font color="0033cc">PFF</font> (l, x, r) ->
        <font color="green">let</font> xl = maximum l <font color="green">in</font>
	<font color="green">let</font> xr = maximum r <font color="green">in</font>
	<font color="green">let</font> l' = remove l <font color="green">in</font>
	<font color="77aaaa">if</font> <font color="0033cc">X</font>.compare xl xr >= 0 <font color="77aaaa">then</font> 
	  p_f l' xl r 
	<font color="77aaaa">else</font> 
	  p_f l' xr (add xl (remove r))
    <font color="990000">(* remove on the right *)</font>
    <font color="77aaaa">|</font> <font color="0033cc">FFF</font> (l, x, r) <font color="77aaaa">|</font> <font color="0033cc">PFP</font> (l, x, r) ->
        <font color="green">let</font> xl = maximum l <font color="green">in</font>
	<font color="green">let</font> xr = maximum r <font color="green">in</font>
	<font color="green">let</font> r' = remove r <font color="green">in</font>
	<font color="77aaaa">if</font> <font color="0033cc">X</font>.compare xl xr > 0 <font color="77aaaa">then</font> 
	  pf_ (add xr (remove l)) xl r'
	<font color="77aaaa">else</font> 
	  pf_ l xr r'

  <font color="green">let</font> <font color="green">rec</font> iter f = <font color="green">function</font>
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font> -> 
	()
    <font color="77aaaa">|</font> <font color="0033cc">FFF</font> (l, x, r) <font color="77aaaa">|</font> <font color="0033cc">PPF</font> (l, x, r) <font color="77aaaa">|</font> <font color="0033cc">PFF</font> (l, x, r) <font color="77aaaa">|</font> <font color="0033cc">PFP</font> (l, x, r) -> 
	iter f l; f x; iter f r

  <font color="green">let</font> <font color="green">rec</font> fold f h x0 = <font color="77aaaa">match</font> h <font color="77aaaa">with</font>
    <font color="77aaaa">|</font> <font color="0033cc">Empty</font> -> 
	x0
    <font color="77aaaa">|</font> <font color="0033cc">FFF</font> (l, x, r) <font color="77aaaa">|</font> <font color="0033cc">PPF</font> (l, x, r) <font color="77aaaa">|</font> <font color="0033cc">PFF</font> (l, x, r) <font color="77aaaa">|</font> <font color="0033cc">PFP</font> (l, x, r) -> 
	fold f l (fold f r (f x x0))

<font color="990099">end</font>
</pre></body></html>
